Nuprl Lemma : reverse-append
11,40
postcript
pdf
T
:Type,
as
,
bs
:(
T
List). rev(
as
@
bs
) ~ (rev(
bs
) @ rev(
as
))
latex
Definitions
A
List
,
[]
,
[
car
/
cdr
]
,
as
@
bs
,
rev(
as
)
,
S
T
,
s
=
t
,
Top
,
x
:
A
.
B
(
x
)
,
t
T
,
Void
,
Type
,
x
:
A
.
B
(
x
)
,
s
~
t
,
x
:
A
B
(
x
)
,
type
List
Lemmas
top
wf
,
member
wf
,
reverse
wf
,
append-nil
,
append
assoc
sq
origin
T:Type, as, bs:(T List). rev(as @ bs) ~ (rev(bs) @ rev(as)) T:Type, as, bs:(T List). rev(as @ bs) ~ (rev(bs) @ rev(as)) 
T
x:A.B(x)
Tx:A. B(x)
B(x)